YES 5.555 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ BR

mainModule List
  ((nub :: (Eq a, Eq b) => [Either b a]  ->  [Either b a]) :: (Eq a, Eq b) => [Either b a]  ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude
  nub :: Eq a => [a]  ->  [a]
nub l = 
nub' l [] where 
nub' [] _ = []
nub' (x : xs) ls 
 | x `elem` ls = 
nub' xs ls
 | otherwise = 
x : nub' xs (x : ls)


module Maybe where
  import qualified List
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR

mainModule List
  ((nub :: (Eq a, Eq b) => [Either b a]  ->  [Either b a]) :: (Eq b, Eq a) => [Either b a]  ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude
  nub :: Eq a => [a]  ->  [a]
nub l = 
nub' l [] where 
nub' [] vw = []
nub' (x : xs) ls 
 | x `elem` ls = 
nub' xs ls
 | otherwise = 
x : nub' xs (x : ls)


module Maybe where
  import qualified List
import qualified Prelude


Cond Reductions:
The following Function with conditions
nub' [] vw = []
nub' (x : xs) ls
 | x `elem` ls
 = nub' xs ls
 | otherwise
 = x : nub' xs (x : ls)

is transformed to
nub' [] vw = nub'3 [] vw
nub' (x : xs) ls = nub'2 (x : xs) ls

nub'0 x xs ls True = x : nub' xs (x : ls)

nub'1 x xs ls True = nub' xs ls
nub'1 x xs ls False = nub'0 x xs ls otherwise

nub'2 (x : xs) ls = nub'1 x xs ls (x `elem` ls)

nub'3 [] vw = []
nub'3 xz yu = nub'2 xz yu

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed

mainModule List
  ((nub :: (Eq b, Eq a) => [Either b a]  ->  [Either b a]) :: (Eq a, Eq b) => [Either b a]  ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude
  nub :: Eq a => [a]  ->  [a]
nub l = 
nub' l [] where 
nub' [] vw = nub'3 [] vw
nub' (x : xs) ls = nub'2 (x : xs) ls
nub'0 x xs ls True = x : nub' xs (x : ls)
nub'1 x xs ls True = nub' xs ls
nub'1 x xs ls False = nub'0 x xs ls otherwise
nub'2 (x : xs) ls = nub'1 x xs ls (x `elem` ls)
nub'3 [] vw = []
nub'3 xz yu = nub'2 xz yu


module Maybe where
  import qualified List
import qualified Prelude


Let/Where Reductions:
The bindings of the following Let/Where expression
nub' l []
where 
nub' [] vw = nub'3 [] vw
nub' (x : xs) ls = nub'2 (x : xs) ls
nub'0 x xs ls True = x : nub' xs (x : ls)
nub'1 x xs ls True = nub' xs ls
nub'1 x xs ls False = nub'0 x xs ls otherwise
nub'2 (x : xs) ls = nub'1 x xs ls (x `elem` ls)
nub'3 [] vw = []
nub'3 xz yu = nub'2 xz yu

are unpacked to the following functions on top level
nubNub'0 x xs ls True = x : nubNub' xs (x : ls)

nubNub' [] vw = nubNub'3 [] vw
nubNub' (x : xs) ls = nubNub'2 (x : xs) ls

nubNub'2 (x : xs) ls = nubNub'1 x xs ls (x `elem` ls)

nubNub'3 [] vw = []
nubNub'3 xz yu = nubNub'2 xz yu

nubNub'1 x xs ls True = nubNub' xs ls
nubNub'1 x xs ls False = nubNub'0 x xs ls otherwise



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow

mainModule List
  (nub :: (Eq b, Eq a) => [Either b a]  ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude
  nub :: Eq a => [a]  ->  [a]
nub l = nubNub' l []

  
nubNub' [] vw = nubNub'3 [] vw
nubNub' (x : xs) ls = nubNub'2 (x : xs) ls

  
nubNub'0 x xs ls True = x : nubNub' xs (x : ls)

  
nubNub'1 x xs ls True = nubNub' xs ls
nubNub'1 x xs ls False = nubNub'0 x xs ls otherwise

  
nubNub'2 (x : xs) ls = nubNub'1 x xs ls (x `elem` ls)

  
nubNub'3 [] vw = []
nubNub'3 xz yu = nubNub'2 xz yu


module Maybe where
  import qualified List
import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yv21800), Succ(yv1900000)) → new_primPlusNat(yv21800, yv1900000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yv186000), Succ(yv190000)) → new_primMulNat(yv186000, Succ(yv190000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yv18600), Succ(yv19000)) → new_primEqNat(yv18600, yv19000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(Right(yv1860), Right(yv1900), cc, app(app(app(ty_@3, dc), dd), de)) → new_esEs3(yv1860, yv1900, dc, dd, de)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), baf, app(ty_Maybe, bcg), bcc) → new_esEs2(yv1861, yv1901, bcg)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(yv1862, yv1902, bbf, bbg, bbh)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), app(app(ty_Either, bdc), bdd), bag, bcc) → new_esEs(yv1860, yv1900, bdc, bdd)
new_esEs2(Just(yv1860), Just(yv1900), app(app(ty_Either, he), hf)) → new_esEs(yv1860, yv1900, he, hf)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), app(app(ty_@2, bde), bdf), bag, bcc) → new_esEs0(yv1860, yv1900, bde, bdf)
new_esEs(Right(yv1860), Right(yv1900), cc, app(ty_[], da)) → new_esEs1(yv1860, yv1900, da)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), baf, bag, app(ty_[], bbd)) → new_esEs1(yv1862, yv1902, bbd)
new_esEs1(:(yv1860, yv1861), :(yv1900, yv1901), gc) → new_esEs1(yv1861, yv1901, gc)
new_esEs0(@2(yv1860, yv1861), @2(yv1900, yv1901), app(ty_[], ff), fb) → new_esEs1(yv1860, yv1900, ff)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), baf, bag, app(app(ty_Either, bah), bba)) → new_esEs(yv1862, yv1902, bah, bba)
new_esEs1(:(yv1860, yv1861), :(yv1900, yv1901), app(ty_[], gh)) → new_esEs1(yv1860, yv1900, gh)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), baf, app(ty_[], bcf), bcc) → new_esEs1(yv1861, yv1901, bcf)
new_esEs2(Just(yv1860), Just(yv1900), app(ty_[], baa)) → new_esEs1(yv1860, yv1900, baa)
new_esEs(Right(yv1860), Right(yv1900), cc, app(app(ty_@2, cf), cg)) → new_esEs0(yv1860, yv1900, cf, cg)
new_esEs2(Just(yv1860), Just(yv1900), app(ty_Maybe, bab)) → new_esEs2(yv1860, yv1900, bab)
new_esEs0(@2(yv1860, yv1861), @2(yv1900, yv1901), app(app(ty_Either, eh), fa), fb) → new_esEs(yv1860, yv1900, eh, fa)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), baf, app(app(ty_@2, bcd), bce), bcc) → new_esEs0(yv1861, yv1901, bcd, bce)
new_esEs(Left(yv1860), Left(yv1900), app(ty_Maybe, bg), bc) → new_esEs2(yv1860, yv1900, bg)
new_esEs0(@2(yv1860, yv1861), @2(yv1900, yv1901), df, app(app(ty_Either, dg), dh)) → new_esEs(yv1861, yv1901, dg, dh)
new_esEs(Left(yv1860), Left(yv1900), app(app(app(ty_@3, bh), ca), cb), bc) → new_esEs3(yv1860, yv1900, bh, ca, cb)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), baf, app(app(app(ty_@3, bch), bda), bdb), bcc) → new_esEs3(yv1861, yv1901, bch, bda, bdb)
new_esEs0(@2(yv1860, yv1861), @2(yv1900, yv1901), df, app(ty_Maybe, ed)) → new_esEs2(yv1861, yv1901, ed)
new_esEs(Right(yv1860), Right(yv1900), cc, app(app(ty_Either, cd), ce)) → new_esEs(yv1860, yv1900, cd, ce)
new_esEs0(@2(yv1860, yv1861), @2(yv1900, yv1901), app(app(app(ty_@3, fh), ga), gb), fb) → new_esEs3(yv1860, yv1900, fh, ga, gb)
new_esEs(Left(yv1860), Left(yv1900), app(app(ty_@2, bd), be), bc) → new_esEs0(yv1860, yv1900, bd, be)
new_esEs1(:(yv1860, yv1861), :(yv1900, yv1901), app(ty_Maybe, ha)) → new_esEs2(yv1860, yv1900, ha)
new_esEs0(@2(yv1860, yv1861), @2(yv1900, yv1901), app(ty_Maybe, fg), fb) → new_esEs2(yv1860, yv1900, fg)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), baf, app(app(ty_Either, bca), bcb), bcc) → new_esEs(yv1861, yv1901, bca, bcb)
new_esEs1(:(yv1860, yv1861), :(yv1900, yv1901), app(app(app(ty_@3, hb), hc), hd)) → new_esEs3(yv1860, yv1900, hb, hc, hd)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), baf, bag, app(ty_Maybe, bbe)) → new_esEs2(yv1862, yv1902, bbe)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), app(ty_Maybe, bdh), bag, bcc) → new_esEs2(yv1860, yv1900, bdh)
new_esEs0(@2(yv1860, yv1861), @2(yv1900, yv1901), app(app(ty_@2, fc), fd), fb) → new_esEs0(yv1860, yv1900, fc, fd)
new_esEs(Right(yv1860), Right(yv1900), cc, app(ty_Maybe, db)) → new_esEs2(yv1860, yv1900, db)
new_esEs(Left(yv1860), Left(yv1900), app(ty_[], bf), bc) → new_esEs1(yv1860, yv1900, bf)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), app(ty_[], bdg), bag, bcc) → new_esEs1(yv1860, yv1900, bdg)
new_esEs0(@2(yv1860, yv1861), @2(yv1900, yv1901), df, app(ty_[], ec)) → new_esEs1(yv1861, yv1901, ec)
new_esEs2(Just(yv1860), Just(yv1900), app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(yv1860, yv1900, bac, bad, bae)
new_esEs0(@2(yv1860, yv1861), @2(yv1900, yv1901), df, app(app(ty_@2, ea), eb)) → new_esEs0(yv1861, yv1901, ea, eb)
new_esEs1(:(yv1860, yv1861), :(yv1900, yv1901), app(app(ty_Either, gd), ge)) → new_esEs(yv1860, yv1900, gd, ge)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), baf, bag, app(app(ty_@2, bbb), bbc)) → new_esEs0(yv1862, yv1902, bbb, bbc)
new_esEs0(@2(yv1860, yv1861), @2(yv1900, yv1901), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(yv1861, yv1901, ee, ef, eg)
new_esEs1(:(yv1860, yv1861), :(yv1900, yv1901), app(app(ty_@2, gf), gg)) → new_esEs0(yv1860, yv1900, gf, gg)
new_esEs(Left(yv1860), Left(yv1900), app(app(ty_Either, ba), bb), bc) → new_esEs(yv1860, yv1900, ba, bb)
new_esEs3(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), app(app(app(ty_@3, bea), beb), bec), bag, bcc) → new_esEs3(yv1860, yv1900, bea, beb, bec)
new_esEs2(Just(yv1860), Just(yv1900), app(app(ty_@2, hg), hh)) → new_esEs0(yv1860, yv1900, hg, hh)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_nubNub'10(yv199, yv200, yv201, yv202, True, yv204, bb) → new_nubNub'(yv200, yv201, yv202, bb)
new_nubNub'1(yv186, yv187, yv188, yv189, yv190, yv191, ba) → new_nubNub'10(yv186, yv187, yv188, yv189, new_esEs4(yv186, yv190, ba), yv191, ba)
new_nubNub'10(yv199, yv200, yv201, yv202, False, :(yv2040, yv2041), bb) → new_nubNub'1(yv199, yv200, yv201, yv202, yv2040, yv2041, bb)
new_nubNub'10(yv199, yv200, yv201, yv202, False, [], bb) → new_nubNub'(yv200, yv199, :(yv201, yv202), bb)
new_nubNub'(:(yv930, yv931), yv94, yv95, bc) → new_nubNub'1(yv930, yv931, yv94, yv95, yv94, yv95, bc)

The TRS R consists of the following rules:

new_esEs18(Just(yv1860), Just(yv1900), ty_Float) → new_esEs15(yv1860, yv1900)
new_esEs18(Just(yv1860), Just(yv1900), ty_Ordering) → new_esEs9(yv1860, yv1900)
new_esEs13(Right(yv1860), Right(yv1900), fh, ty_Integer) → new_esEs10(yv1860, yv1900)
new_esEs21(yv1860, yv1900, ty_Float) → new_esEs15(yv1860, yv1900)
new_esEs21(yv1860, yv1900, app(ty_[], fa)) → new_esEs7(yv1860, yv1900, fa)
new_esEs4(yv186, yv190, ty_Bool) → new_esEs14(yv186, yv190)
new_primPlusNat1(Succ(yv21800), Succ(yv1900000)) → Succ(Succ(new_primPlusNat1(yv21800, yv1900000)))
new_esEs21(yv1860, yv1900, ty_Double) → new_esEs17(yv1860, yv1900)
new_primEqInt(Neg(Succ(yv18600)), Pos(yv1900)) → False
new_primEqInt(Pos(Succ(yv18600)), Neg(yv1900)) → False
new_esEs8(yv1860, yv1900, app(app(ty_Either, bf), bg)) → new_esEs13(yv1860, yv1900, bf, bg)
new_esEs9(LT, GT) → False
new_esEs9(GT, LT) → False
new_esEs24(yv1862, yv1902, app(app(ty_@2, ha), hb)) → new_esEs16(yv1862, yv1902, ha, hb)
new_primEqInt(Neg(Zero), Pos(Succ(yv19000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yv19000))) → False
new_esEs21(yv1860, yv1900, ty_Char) → new_esEs11(yv1860, yv1900)
new_esEs13(Left(yv1860), Left(yv1900), app(app(ty_Either, bdg), bdh), ga) → new_esEs13(yv1860, yv1900, bdg, bdh)
new_esEs13(Left(yv1860), Left(yv1900), ty_Ordering, ga) → new_esEs9(yv1860, yv1900)
new_esEs24(yv1862, yv1902, app(ty_Maybe, hd)) → new_esEs18(yv1862, yv1902, hd)
new_esEs8(yv1860, yv1900, ty_@0) → new_esEs5(yv1860, yv1900)
new_esEs25(yv1861, yv1901, ty_Float) → new_esEs15(yv1861, yv1901)
new_esEs26(yv1860, yv1900, ty_Char) → new_esEs11(yv1860, yv1900)
new_primMulNat0(Zero, Zero) → Zero
new_esEs26(yv1860, yv1900, ty_Float) → new_esEs15(yv1860, yv1900)
new_esEs4(yv186, yv190, app(ty_[], bd)) → new_esEs7(yv186, yv190, bd)
new_esEs25(yv1861, yv1901, app(app(ty_@2, bac), bad)) → new_esEs16(yv1861, yv1901, bac, bad)
new_esEs8(yv1860, yv1900, ty_Double) → new_esEs17(yv1860, yv1900)
new_primPlusNat0(Zero, yv190000) → Succ(yv190000)
new_esEs13(Right(yv1860), Right(yv1900), fh, app(app(app(ty_@3, bfg), bfh), bga)) → new_esEs19(yv1860, yv1900, bfg, bfh, bga)
new_esEs13(Left(yv1860), Left(yv1900), ty_@0, ga) → new_esEs5(yv1860, yv1900)
new_esEs9(GT, GT) → True
new_esEs4(yv186, yv190, ty_Float) → new_esEs15(yv186, yv190)
new_esEs13(Left(yv1860), Left(yv1900), app(ty_[], bec), ga) → new_esEs7(yv1860, yv1900, bec)
new_esEs20(yv1861, yv1901, ty_Integer) → new_esEs10(yv1861, yv1901)
new_esEs21(yv1860, yv1900, ty_Int) → new_esEs6(yv1860, yv1900)
new_esEs13(Left(yv1860), Left(yv1900), ty_Char, ga) → new_esEs11(yv1860, yv1900)
new_esEs26(yv1860, yv1900, ty_Bool) → new_esEs14(yv1860, yv1900)
new_esEs8(yv1860, yv1900, ty_Bool) → new_esEs14(yv1860, yv1900)
new_esEs17(Double(yv1860, yv1861), Double(yv1900, yv1901)) → new_esEs6(new_sr(yv1860, yv1900), new_sr(yv1861, yv1901))
new_esEs4(yv186, yv190, ty_Char) → new_esEs11(yv186, yv190)
new_esEs18(Just(yv1860), Just(yv1900), ty_Integer) → new_esEs10(yv1860, yv1900)
new_esEs25(yv1861, yv1901, ty_Integer) → new_esEs10(yv1861, yv1901)
new_esEs20(yv1861, yv1901, ty_Int) → new_esEs6(yv1861, yv1901)
new_sr(Neg(yv18600), Pos(yv19000)) → Neg(new_primMulNat0(yv18600, yv19000))
new_sr(Pos(yv18600), Neg(yv19000)) → Neg(new_primMulNat0(yv18600, yv19000))
new_esEs20(yv1861, yv1901, ty_@0) → new_esEs5(yv1861, yv1901)
new_esEs13(Right(yv1860), Right(yv1900), fh, ty_Char) → new_esEs11(yv1860, yv1900)
new_esEs13(Left(yv1860), Left(yv1900), app(ty_Ratio, bdf), ga) → new_esEs12(yv1860, yv1900, bdf)
new_esEs18(Just(yv1860), Just(yv1900), ty_Char) → new_esEs11(yv1860, yv1900)
new_esEs24(yv1862, yv1902, app(app(app(ty_@3, he), hf), hg)) → new_esEs19(yv1862, yv1902, he, hf, hg)
new_esEs12(:%(yv1860, yv1861), :%(yv1900, yv1901), fg) → new_asAs(new_esEs23(yv1860, yv1900, fg), new_esEs22(yv1861, yv1901, fg))
new_esEs6(yv186, yv190) → new_primEqInt(yv186, yv190)
new_esEs13(Right(yv1860), Right(yv1900), fh, app(app(ty_@2, bfc), bfd)) → new_esEs16(yv1860, yv1900, bfc, bfd)
new_esEs19(@3(yv1860, yv1861, yv1862), @3(yv1900, yv1901, yv1902), gc, gd, ge) → new_asAs(new_esEs26(yv1860, yv1900, gc), new_asAs(new_esEs25(yv1861, yv1901, gd), new_esEs24(yv1862, yv1902, ge)))
new_esEs25(yv1861, yv1901, app(ty_[], bae)) → new_esEs7(yv1861, yv1901, bae)
new_esEs23(yv1860, yv1900, ty_Integer) → new_esEs10(yv1860, yv1900)
new_esEs20(yv1861, yv1901, app(app(ty_Either, dc), dd)) → new_esEs13(yv1861, yv1901, dc, dd)
new_esEs25(yv1861, yv1901, ty_Int) → new_esEs6(yv1861, yv1901)
new_esEs4(yv186, yv190, app(app(app(ty_@3, gc), gd), ge)) → new_esEs19(yv186, yv190, gc, gd, ge)
new_esEs13(Left(yv1860), Left(yv1900), ty_Float, ga) → new_esEs15(yv1860, yv1900)
new_esEs8(yv1860, yv1900, ty_Int) → new_esEs6(yv1860, yv1900)
new_esEs7([], [], bd) → True
new_esEs20(yv1861, yv1901, app(app(ty_@2, de), df)) → new_esEs16(yv1861, yv1901, de, df)
new_esEs20(yv1861, yv1901, ty_Char) → new_esEs11(yv1861, yv1901)
new_esEs22(yv1861, yv1901, ty_Integer) → new_esEs10(yv1861, yv1901)
new_esEs26(yv1860, yv1900, ty_@0) → new_esEs5(yv1860, yv1900)
new_primEqNat0(Zero, Succ(yv19000)) → False
new_primEqNat0(Succ(yv18600), Zero) → False
new_esEs21(yv1860, yv1900, app(app(app(ty_@3, fc), fd), ff)) → new_esEs19(yv1860, yv1900, fc, fd, ff)
new_esEs20(yv1861, yv1901, ty_Bool) → new_esEs14(yv1861, yv1901)
new_esEs18(Just(yv1860), Just(yv1900), ty_Double) → new_esEs17(yv1860, yv1900)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs21(yv1860, yv1900, ty_Integer) → new_esEs10(yv1860, yv1900)
new_esEs10(Integer(yv1860), Integer(yv1900)) → new_primEqInt(yv1860, yv1900)
new_esEs26(yv1860, yv1900, app(ty_Maybe, bbh)) → new_esEs18(yv1860, yv1900, bbh)
new_esEs8(yv1860, yv1900, app(ty_Maybe, cc)) → new_esEs18(yv1860, yv1900, cc)
new_esEs25(yv1861, yv1901, ty_Char) → new_esEs11(yv1861, yv1901)
new_esEs13(Left(yv1860), Left(yv1900), app(app(ty_@2, bea), beb), ga) → new_esEs16(yv1860, yv1900, bea, beb)
new_esEs5(@0, @0) → True
new_esEs13(Right(yv1860), Right(yv1900), fh, app(ty_Maybe, bff)) → new_esEs18(yv1860, yv1900, bff)
new_esEs15(Float(yv1860, yv1861), Float(yv1900, yv1901)) → new_esEs6(new_sr(yv1860, yv1900), new_sr(yv1861, yv1901))
new_esEs25(yv1861, yv1901, ty_Bool) → new_esEs14(yv1861, yv1901)
new_esEs18(Just(yv1860), Just(yv1900), app(ty_Ratio, bcd)) → new_esEs12(yv1860, yv1900, bcd)
new_esEs20(yv1861, yv1901, app(ty_Ratio, db)) → new_esEs12(yv1861, yv1901, db)
new_esEs16(@2(yv1860, yv1861), @2(yv1900, yv1901), cg, da) → new_asAs(new_esEs21(yv1860, yv1900, cg), new_esEs20(yv1861, yv1901, da))
new_esEs23(yv1860, yv1900, ty_Int) → new_esEs6(yv1860, yv1900)
new_esEs7(:(yv1860, yv1861), [], bd) → False
new_esEs7([], :(yv1900, yv1901), bd) → False
new_esEs8(yv1860, yv1900, ty_Integer) → new_esEs10(yv1860, yv1900)
new_esEs9(EQ, GT) → False
new_esEs9(GT, EQ) → False
new_esEs13(Right(yv1860), Right(yv1900), fh, ty_Int) → new_esEs6(yv1860, yv1900)
new_esEs13(Right(yv1860), Right(yv1900), fh, ty_@0) → new_esEs5(yv1860, yv1900)
new_esEs13(Left(yv1860), Left(yv1900), ty_Int, ga) → new_esEs6(yv1860, yv1900)
new_esEs18(Nothing, Nothing, gb) → True
new_esEs21(yv1860, yv1900, ty_Bool) → new_esEs14(yv1860, yv1900)
new_esEs11(Char(yv1860), Char(yv1900)) → new_primEqNat0(yv1860, yv1900)
new_esEs8(yv1860, yv1900, ty_Ordering) → new_esEs9(yv1860, yv1900)
new_esEs26(yv1860, yv1900, ty_Int) → new_esEs6(yv1860, yv1900)
new_esEs26(yv1860, yv1900, ty_Double) → new_esEs17(yv1860, yv1900)
new_esEs18(Just(yv1860), Just(yv1900), app(ty_[], bda)) → new_esEs7(yv1860, yv1900, bda)
new_esEs18(Just(yv1860), Just(yv1900), app(app(ty_Either, bce), bcf)) → new_esEs13(yv1860, yv1900, bce, bcf)
new_esEs26(yv1860, yv1900, app(ty_[], bbg)) → new_esEs7(yv1860, yv1900, bbg)
new_esEs8(yv1860, yv1900, ty_Char) → new_esEs11(yv1860, yv1900)
new_esEs21(yv1860, yv1900, app(app(ty_@2, eg), eh)) → new_esEs16(yv1860, yv1900, eg, eh)
new_esEs25(yv1861, yv1901, ty_@0) → new_esEs5(yv1861, yv1901)
new_esEs26(yv1860, yv1900, app(app(ty_@2, bbe), bbf)) → new_esEs16(yv1860, yv1900, bbe, bbf)
new_esEs25(yv1861, yv1901, ty_Double) → new_esEs17(yv1861, yv1901)
new_esEs20(yv1861, yv1901, app(app(app(ty_@3, ea), eb), ec)) → new_esEs19(yv1861, yv1901, ea, eb, ec)
new_sr(Neg(yv18600), Neg(yv19000)) → Pos(new_primMulNat0(yv18600, yv19000))
new_esEs24(yv1862, yv1902, ty_Char) → new_esEs11(yv1862, yv1902)
new_esEs8(yv1860, yv1900, app(ty_Ratio, be)) → new_esEs12(yv1860, yv1900, be)
new_sr(Pos(yv18600), Pos(yv19000)) → Pos(new_primMulNat0(yv18600, yv19000))
new_asAs(False, yv217) → False
new_esEs4(yv186, yv190, app(ty_Ratio, fg)) → new_esEs12(yv186, yv190, fg)
new_primEqNat0(Zero, Zero) → True
new_esEs24(yv1862, yv1902, ty_Int) → new_esEs6(yv1862, yv1902)
new_esEs21(yv1860, yv1900, app(ty_Maybe, fb)) → new_esEs18(yv1860, yv1900, fb)
new_primMulNat0(Zero, Succ(yv190000)) → Zero
new_primMulNat0(Succ(yv186000), Zero) → Zero
new_esEs18(Just(yv1860), Just(yv1900), ty_Bool) → new_esEs14(yv1860, yv1900)
new_esEs13(Left(yv1860), Left(yv1900), ty_Integer, ga) → new_esEs10(yv1860, yv1900)
new_esEs18(Just(yv1860), Nothing, gb) → False
new_esEs18(Nothing, Just(yv1900), gb) → False
new_esEs24(yv1862, yv1902, ty_@0) → new_esEs5(yv1862, yv1902)
new_esEs13(Right(yv1860), Right(yv1900), fh, ty_Float) → new_esEs15(yv1860, yv1900)
new_esEs21(yv1860, yv1900, ty_@0) → new_esEs5(yv1860, yv1900)
new_esEs4(yv186, yv190, ty_Int) → new_esEs6(yv186, yv190)
new_esEs20(yv1861, yv1901, ty_Double) → new_esEs17(yv1861, yv1901)
new_esEs8(yv1860, yv1900, app(ty_[], cb)) → new_esEs7(yv1860, yv1900, cb)
new_primPlusNat0(Succ(yv2180), yv190000) → Succ(Succ(new_primPlusNat1(yv2180, yv190000)))
new_esEs24(yv1862, yv1902, ty_Integer) → new_esEs10(yv1862, yv1902)
new_esEs14(True, True) → True
new_esEs18(Just(yv1860), Just(yv1900), app(app(ty_@2, bcg), bch)) → new_esEs16(yv1860, yv1900, bcg, bch)
new_esEs24(yv1862, yv1902, ty_Double) → new_esEs17(yv1862, yv1902)
new_esEs20(yv1861, yv1901, ty_Ordering) → new_esEs9(yv1861, yv1901)
new_esEs26(yv1860, yv1900, app(ty_Ratio, bbb)) → new_esEs12(yv1860, yv1900, bbb)
new_esEs21(yv1860, yv1900, ty_Ordering) → new_esEs9(yv1860, yv1900)
new_esEs4(yv186, yv190, ty_Integer) → new_esEs10(yv186, yv190)
new_esEs9(EQ, EQ) → True
new_esEs8(yv1860, yv1900, ty_Float) → new_esEs15(yv1860, yv1900)
new_primEqInt(Neg(Succ(yv18600)), Neg(Succ(yv19000))) → new_primEqNat0(yv18600, yv19000)
new_esEs25(yv1861, yv1901, app(app(app(ty_@3, bag), bah), bba)) → new_esEs19(yv1861, yv1901, bag, bah, bba)
new_esEs4(yv186, yv190, ty_Double) → new_esEs17(yv186, yv190)
new_esEs13(Left(yv1860), Right(yv1900), fh, ga) → False
new_esEs13(Right(yv1860), Left(yv1900), fh, ga) → False
new_esEs13(Right(yv1860), Right(yv1900), fh, app(app(ty_Either, bfa), bfb)) → new_esEs13(yv1860, yv1900, bfa, bfb)
new_esEs24(yv1862, yv1902, ty_Bool) → new_esEs14(yv1862, yv1902)
new_primPlusNat1(Zero, Succ(yv1900000)) → Succ(yv1900000)
new_primPlusNat1(Succ(yv21800), Zero) → Succ(yv21800)
new_esEs9(LT, EQ) → False
new_esEs9(EQ, LT) → False
new_esEs18(Just(yv1860), Just(yv1900), app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs19(yv1860, yv1900, bdc, bdd, bde)
new_esEs8(yv1860, yv1900, app(app(app(ty_@3, cd), ce), cf)) → new_esEs19(yv1860, yv1900, cd, ce, cf)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs13(Right(yv1860), Right(yv1900), fh, ty_Ordering) → new_esEs9(yv1860, yv1900)
new_esEs4(yv186, yv190, app(app(ty_Either, fh), ga)) → new_esEs13(yv186, yv190, fh, ga)
new_esEs20(yv1861, yv1901, app(ty_[], dg)) → new_esEs7(yv1861, yv1901, dg)
new_esEs13(Left(yv1860), Left(yv1900), app(ty_Maybe, bed), ga) → new_esEs18(yv1860, yv1900, bed)
new_esEs14(False, False) → True
new_primEqInt(Neg(Zero), Neg(Succ(yv19000))) → False
new_primEqInt(Neg(Succ(yv18600)), Neg(Zero)) → False
new_esEs25(yv1861, yv1901, ty_Ordering) → new_esEs9(yv1861, yv1901)
new_esEs24(yv1862, yv1902, app(app(ty_Either, gg), gh)) → new_esEs13(yv1862, yv1902, gg, gh)
new_esEs24(yv1862, yv1902, ty_Ordering) → new_esEs9(yv1862, yv1902)
new_esEs21(yv1860, yv1900, app(app(ty_Either, ee), ef)) → new_esEs13(yv1860, yv1900, ee, ef)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs26(yv1860, yv1900, ty_Ordering) → new_esEs9(yv1860, yv1900)
new_esEs18(Just(yv1860), Just(yv1900), ty_@0) → new_esEs5(yv1860, yv1900)
new_asAs(True, yv217) → yv217
new_esEs7(:(yv1860, yv1861), :(yv1900, yv1901), bd) → new_asAs(new_esEs8(yv1860, yv1900, bd), new_esEs7(yv1861, yv1901, bd))
new_primMulNat0(Succ(yv186000), Succ(yv190000)) → new_primPlusNat0(new_primMulNat0(yv186000, Succ(yv190000)), yv190000)
new_esEs13(Left(yv1860), Left(yv1900), app(app(app(ty_@3, bee), bef), beg), ga) → new_esEs19(yv1860, yv1900, bee, bef, beg)
new_esEs25(yv1861, yv1901, app(app(ty_Either, baa), bab)) → new_esEs13(yv1861, yv1901, baa, bab)
new_primEqInt(Pos(Succ(yv18600)), Pos(Succ(yv19000))) → new_primEqNat0(yv18600, yv19000)
new_esEs20(yv1861, yv1901, app(ty_Maybe, dh)) → new_esEs18(yv1861, yv1901, dh)
new_esEs26(yv1860, yv1900, ty_Integer) → new_esEs10(yv1860, yv1900)
new_esEs4(yv186, yv190, ty_Ordering) → new_esEs9(yv186, yv190)
new_esEs14(True, False) → False
new_esEs14(False, True) → False
new_esEs26(yv1860, yv1900, app(app(app(ty_@3, bca), bcb), bcc)) → new_esEs19(yv1860, yv1900, bca, bcb, bcc)
new_esEs24(yv1862, yv1902, app(ty_[], hc)) → new_esEs7(yv1862, yv1902, hc)
new_primEqNat0(Succ(yv18600), Succ(yv19000)) → new_primEqNat0(yv18600, yv19000)
new_esEs4(yv186, yv190, app(app(ty_@2, cg), da)) → new_esEs16(yv186, yv190, cg, da)
new_esEs21(yv1860, yv1900, app(ty_Ratio, ed)) → new_esEs12(yv1860, yv1900, ed)
new_esEs13(Right(yv1860), Right(yv1900), fh, app(ty_Ratio, beh)) → new_esEs12(yv1860, yv1900, beh)
new_esEs4(yv186, yv190, ty_@0) → new_esEs5(yv186, yv190)
new_esEs22(yv1861, yv1901, ty_Int) → new_esEs6(yv1861, yv1901)
new_esEs9(LT, LT) → True
new_esEs24(yv1862, yv1902, app(ty_Ratio, gf)) → new_esEs12(yv1862, yv1902, gf)
new_esEs13(Left(yv1860), Left(yv1900), ty_Double, ga) → new_esEs17(yv1860, yv1900)
new_esEs18(Just(yv1860), Just(yv1900), ty_Int) → new_esEs6(yv1860, yv1900)
new_esEs20(yv1861, yv1901, ty_Float) → new_esEs15(yv1861, yv1901)
new_esEs8(yv1860, yv1900, app(app(ty_@2, bh), ca)) → new_esEs16(yv1860, yv1900, bh, ca)
new_esEs13(Right(yv1860), Right(yv1900), fh, app(ty_[], bfe)) → new_esEs7(yv1860, yv1900, bfe)
new_esEs18(Just(yv1860), Just(yv1900), app(ty_Maybe, bdb)) → new_esEs18(yv1860, yv1900, bdb)
new_primEqInt(Pos(Zero), Pos(Succ(yv19000))) → False
new_primEqInt(Pos(Succ(yv18600)), Pos(Zero)) → False
new_esEs13(Right(yv1860), Right(yv1900), fh, ty_Bool) → new_esEs14(yv1860, yv1900)
new_esEs25(yv1861, yv1901, app(ty_Ratio, hh)) → new_esEs12(yv1861, yv1901, hh)
new_esEs26(yv1860, yv1900, app(app(ty_Either, bbc), bbd)) → new_esEs13(yv1860, yv1900, bbc, bbd)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs25(yv1861, yv1901, app(ty_Maybe, baf)) → new_esEs18(yv1861, yv1901, baf)
new_esEs24(yv1862, yv1902, ty_Float) → new_esEs15(yv1862, yv1902)
new_esEs13(Right(yv1860), Right(yv1900), fh, ty_Double) → new_esEs17(yv1860, yv1900)
new_esEs13(Left(yv1860), Left(yv1900), ty_Bool, ga) → new_esEs14(yv1860, yv1900)
new_esEs4(yv186, yv190, app(ty_Maybe, gb)) → new_esEs18(yv186, yv190, gb)

The set Q consists of the following terms:

new_esEs13(Right(x0), Right(x1), x2, ty_Bool)
new_esEs21(x0, x1, ty_Integer)
new_esEs13(Left(x0), Left(x1), ty_Float, x2)
new_esEs16(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(GT, GT)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(@0, @0)
new_esEs18(Just(x0), Just(x1), app(ty_[], x2))
new_esEs4(x0, x1, ty_Char)
new_esEs18(Just(x0), Just(x1), ty_Ordering)
new_esEs24(x0, x1, ty_Float)
new_primPlusNat0(Succ(x0), x1)
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_esEs18(Just(x0), Just(x1), ty_Integer)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, ty_@0)
new_esEs7(:(x0, x1), :(x2, x3), x4)
new_esEs25(x0, x1, ty_Ordering)
new_esEs13(Right(x0), Right(x1), x2, ty_@0)
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Int)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs18(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs13(Right(x0), Right(x1), x2, ty_Integer)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs24(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_@0)
new_primMulNat0(Succ(x0), Zero)
new_esEs9(EQ, EQ)
new_esEs26(x0, x1, ty_Ordering)
new_esEs13(Left(x0), Left(x1), ty_Integer, x2)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs18(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Bool)
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(:%(x0, x1), :%(x2, x3), x4)
new_esEs14(False, True)
new_esEs14(True, False)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Integer)
new_sr(Neg(x0), Neg(x1))
new_esEs21(x0, x1, ty_Char)
new_esEs13(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs18(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Float)
new_esEs7([], :(x0, x1), x2)
new_esEs9(GT, LT)
new_esEs9(LT, GT)
new_esEs22(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_esEs6(x0, x1)
new_primMulNat0(Zero, Succ(x0))
new_esEs18(Just(x0), Just(x1), ty_Bool)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(Just(x0), Just(x1), ty_Char)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs13(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs13(Right(x0), Right(x1), x2, ty_Double)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs9(EQ, GT)
new_esEs9(GT, EQ)
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(Just(x0), Just(x1), ty_@0)
new_esEs8(x0, x1, ty_Int)
new_esEs18(Nothing, Just(x0), x1)
new_esEs26(x0, x1, ty_@0)
new_esEs8(x0, x1, ty_@0)
new_esEs26(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Char)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs14(True, True)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(Just(x0), Just(x1), ty_Double)
new_esEs20(x0, x1, ty_Integer)
new_esEs13(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Double)
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs18(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs7([], [], x0)
new_esEs13(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, ty_Float)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs13(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs19(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs8(x0, x1, ty_Float)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat0(Zero, Zero)
new_esEs21(x0, x1, ty_Bool)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs13(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs13(Left(x0), Left(x1), ty_Bool, x2)
new_esEs8(x0, x1, ty_Ordering)
new_esEs13(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, ty_Int)
new_esEs17(Double(x0, x1), Double(x2, x3))
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_@0)
new_esEs26(x0, x1, ty_Bool)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, ty_Int)
new_esEs13(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs26(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_esEs4(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Char)
new_esEs13(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs4(x0, x1, ty_Ordering)
new_asAs(True, x0)
new_esEs11(Char(x0), Char(x1))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs9(EQ, LT)
new_esEs9(LT, EQ)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs8(x0, x1, ty_Double)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs18(Just(x0), Nothing, x1)
new_esEs18(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Double)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Ordering)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_@0)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs7(:(x0, x1), [], x2)
new_esEs13(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs13(Left(x0), Left(x1), ty_@0, x2)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Ordering)
new_esEs13(Right(x0), Left(x1), x2, x3)
new_esEs13(Left(x0), Right(x1), x2, x3)
new_primPlusNat1(Zero, Succ(x0))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Left(x0), Left(x1), ty_Int, x2)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(x0, x1, ty_Char)
new_primPlusNat1(Zero, Zero)
new_esEs18(Just(x0), Just(x1), ty_Int)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Double)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs18(Just(x0), Just(x1), ty_Float)
new_esEs13(Left(x0), Left(x1), ty_Char, x2)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, ty_Double)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Float)
new_esEs8(x0, x1, ty_Bool)
new_esEs4(x0, x1, ty_@0)
new_esEs14(False, False)
new_primEqInt(Pos(Zero), Pos(Zero))
new_asAs(False, x0)
new_esEs8(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Bool)
new_esEs13(Right(x0), Right(x1), x2, ty_Float)
new_esEs18(Nothing, Nothing, x0)
new_esEs10(Integer(x0), Integer(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs9(LT, LT)
new_primEqNat0(Succ(x0), Zero)
new_esEs4(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(ty_Ratio, x2))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: